Maybe squashing the commits would make sense as this originates from some unrelated branch, the contents of which were merged or discarded already.

@mezpusz - any reason for this to be on hold? Looks like something we want.

There was a slight performance worsening (<10 problems lost), so it was just left as undecided. I can rerun it to see how it goes now.

Thanks for the update! It would be good to work out what went wrong with those 10 problems. Otherwise I'm happy to merge.

Currently it's just one problem lost for Discount, none for Otter over FOL with -i 20000, but there is an increase in instructions spent/runtime apparently:

Discount:

run 0 unsat: 9208 (1) sat: 1030 (0) cputime: 56704.85 s instructions: 222910720 Mi memory: 1533982.30 MB
run 1 unsat: 9207 (0) sat: 1030 (0) cputime: 57026.97 s instructions: 222964103 Mi memory: 1529041.49 MB

Otter:

run 0 unsat: 9312 (0) sat: 1020 (0) cputime: 61537.83 s instructions: 222902233 Mi memory: 1739725.78 MB
run 1 unsat: 9312 (0) sat: 1020 (0) cputime: 61743.87 s instructions: 222978995 Mi memory: 1731210.00 MB

The problem lost is LCL/LCL640+1.015.p, and it is solved with 153 extra megainstructions.

So... 🤷

Then...I don't care personally, @quickbeam123 ?

Sure, let's go! We need more code trees :)

Can you cleanup the history where it would make sense, @mezpusz ? Then I'm happy to merge.

@MichaelRawson can you please "squash and merge" the PR? I'm okay with having just one commit, and locally it seems to be hellish to do.

Gross - I usually just rebase onto master and then merge, but I hadn't encountered this particular scenario before. 🤷 I'll work out how to do it properly for next time. Thanks!

(please do claim credit - git commit --amend --reset-author and then force-push)

Merged.

No worries, and thanks for the merge. This branch was a bit cursed anyways, I'll try to organize changes a bit more tidily next time. 😀